FDL - Nuprl Lemma : decidable__rel_star-causl

Nuprl Lemma : decidable__rel_star-causl

es:ES, R:(E

E

).
(

x, y:E. (R(x,y))

(x < y))

(

x, y:E. Dec(R(x,y)))

(

y, x:E. Dec((R^*)(x,y)))

Definitions P & Q, P Q, x f y, P Q, P Q, t T, P Q, , x:A. B(x)

Lemmas event system wf, es-causl wf, decidable wf, es-E wf, decidable es-E-equal, decidable or, rel-star-iff-rel-plus-or, rel plus wf, rel star wf, decidable functionality, decidable rel plus-causl